/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.generator.util;

import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;

import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.generator.ArneGeneratorPlugin;
import nl.cwi.arne.lts.util.LTSFileIndex;
import nl.cwi.arne.mcrl2.toolchains.CompareLTSToolChain;
import nl.cwi.arne.mcrl2.util.MCRL2Options.Equivalence;

import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.Status;

/**
 * @author Christian Krause
 */
public class ActivationEquivalenceClasses extends LinkedHashMap<NetworkActivation,List<NetworkActivation>> {

	// Default serial ID.
	private static final long serialVersionUID = 1L;
	
	// LTS file index.
	private LTSFileIndex fileIndex;
	
	// LTS file map.
	private Map<File,NetworkActivation> fileMap;
	
	// Equivalence type.
	private Equivalence equivalence;
	
	// Equivalence classes stored in a list (without duplicates).
	private List<List<NetworkActivation>> classes;
	
	/**
	 * Default constructor.
	 * @param equivalence Equivalence type.
	 */
	public ActivationEquivalenceClasses(Equivalence equivalence) {
		this.equivalence = equivalence;
		this.fileIndex = new LTSFileIndex();
		this.fileMap = new HashMap<File,NetworkActivation>();
		this.classes = new ArrayList<List<NetworkActivation>>();
	}
	
	/**
	 * Add a network activation to the equivalence classes.
	 * Returns the updated equivalence class for the activation.
	 * If no class exists yet, a new one is created with the 
	 * activation in it.
	 * 
	 * @param activation The network activation.
	 * @param lts The corresponding LTS.
	 * @param numStates Number of states in the LTS.
	 * @param numTransitions Number of transitions in the LTS.
	 * @return The equivalence class.
	 */
	public List<NetworkActivation> add(NetworkActivation activation, File lts, int numStates, int numTransitions) {
		
		// Find an equivalent LTS file:
		List<File> files = fileIndex.get(numStates, numTransitions);
		File equivalent = null;
		for (File lts2 : files) {
			if (doCompare(lts,lts2)==true) {
				equivalent = lts2;
				break;
			}
		}
		
		// Did we find an equivalence network activation?
		if (equivalent!=null) {
			List<NetworkActivation> clazz = get(fileMap.get(equivalent));
			put(activation,clazz);
		} else {
			List<NetworkActivation> clazz = new ArrayList<NetworkActivation>();
			put(activation, clazz);
			classes.add(clazz);
			files.add(lts);
		}
		
		// Get the equivalence class and add the activation.
		List<NetworkActivation> clazz = get(activation);
		clazz.add(activation);	

		// Associate the LTS to the activation:
		fileMap.put(lts, activation);
		
		// Done.
		return clazz;
		
	}
	
	public LTSFileIndex getLTSFileIndex() {
		return fileIndex;
	}
	
	@Override
    public Collection<List<NetworkActivation>> values() {
		return Collections.unmodifiableCollection(classes);
    }
	
	public IStatus verify(IProgressMonitor monitor) {
		
		monitor.beginTask("Verifying equivalence classes..", classes.size()*2);
		
		// First check if the elements in every equivalence class are actually equivalent.
		for (List<NetworkActivation> clazz : classes) {
			File last = getLTSFile(clazz.get(0));
			for (int i=1; i<clazz.size(); i++) {
				File current = getLTSFile(clazz.get(i));
				if (doCompare(last,current)==false) {
					return new Status(IStatus.ERROR, ArneGeneratorPlugin.PLUGIN_ID, "Equivalence class (" + i + ") contains inequivalent LTSs");
				}
				last = current;
			}
			monitor.worked(1);
		}
		
		// Now check if the classes are disjoint:
		for (int i=1; i<classes.size(); i++) {
			File lts1 = getLTSFile(classes.get(i-1).get(0));
			File lts2 = getLTSFile(classes.get(i).get(0));
			if (doCompare(lts1,lts2)==true) {
				return new Status(IStatus.ERROR, ArneGeneratorPlugin.PLUGIN_ID, "Equivalences class (" + i + ") and (" + (i-1) + " are not disjoint");
			}
			monitor.worked(1);
		}
		
		monitor.done();
		return Status.OK_STATUS;
	}
	
	private File getLTSFile(NetworkActivation activation) {
		for (Map.Entry<File,NetworkActivation> entry : fileMap.entrySet()) {
			if (entry.getValue()==activation) return entry.getKey();
		}
		return null;
	}
	
	private boolean doCompare(File lts1, File lts2) {
		CompareLTSToolChain compare = new CompareLTSToolChain(lts1, lts2, equivalence);
		IStatus status = compare.execute(new NullProgressMonitor());
		if (status.getSeverity()!=IStatus.OK) {
			throw new RuntimeException(status.getMessage());
		}
		return compare.getResult();
	}
	
	public void saveLTSs(File folder) throws IOException {
		if (!folder.exists()) {
			folder.mkdirs();
		}
		for (int i=0; i<classes.size(); i++) {
			List<NetworkActivation> clazz = classes.get(i);
			File subFolder = new File(folder.getAbsolutePath() + File.separator + i);
			if (!subFolder.exists()) {
				subFolder.mkdir();
			}
			for (int j=0; j<clazz.size(); j++) {
				File autFile = new File(subFolder.getAbsolutePath() + File.separator + j + ".aut");
				copyFile(getLTSFile(clazz.get(j)), autFile);
			}
		}
		
	}
	
	private void copyFile(File source, File target) throws IOException {
		InputStream in = new FileInputStream(source);
		OutputStream out = new FileOutputStream(target);
		byte[] buf = new byte[1024];
		int len;
		while ((len = in.read(buf))>0){
			out.write(buf, 0, len);
		}
		in.close();
		out.close();
	}
	
}
